Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    f(x,g(y))  → f(h(x),i(x,y))
2:    i(x,j(0,0))  → g(0)
3:    i(x,j(y,z))  → j(g(y),i(x,z))
4:    i(h(x),j(j(y,z),0))  → j(i(h(x),j(y,z)),i(x,j(y,z)))
5:    j(g(x),g(y))  → g(j(x,y))
There are 8 dependency pairs:
6:    F(x,g(y))  → F(h(x),i(x,y))
7:    F(x,g(y))  → I(x,y)
8:    I(x,j(y,z))  → J(g(y),i(x,z))
9:    I(x,j(y,z))  → I(x,z)
10:    I(h(x),j(j(y,z),0))  → J(i(h(x),j(y,z)),i(x,j(y,z)))
11:    I(h(x),j(j(y,z),0))  → I(h(x),j(y,z))
12:    I(h(x),j(j(y,z),0))  → I(x,j(y,z))
13:    J(g(x),g(y))  → J(x,y)
The approximated dependency graph contains 3 SCCs: {13}, {9,11,12} and {6}.
Tyrolean Termination Tool  (0.09 seconds)   ---  May 3, 2006